Verification systems play an important role in the design of complex systems in allowing for the automated testing of the underlying system design and the identification of potentially unsound constructs. Nuprl is a well-known interactive theorem-proving system, see, e.g., R. L. Constable et al., Implementing Mathematics with Nuprl Proof Development System, Prentice-Hall, Inc., Englewood Cliffs, N.J. 1986, employed in verification tools which has proven to be highly effective in a variety of applications. See, for example, P. B. Jackson, Exploring Abstract Algebra in Constructive Type Theory, In 12.sup.th Conference on Automated Deduction, Springer, June 1994. Briefly, Nuprl is a computer system that supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics. One of the important features of Nuprl is that the system's logic takes account of computational meaning of assertions and proofs. Thus, the system is sensitive to the computational meaning of terms, assertions, and proofs, and the system can carry out the actions used to define such computational meaning.
Typically, users of Nuprl (and verification systems employing Nuprl) verify applications, e.g. protocols, by interacting with the system to construct a formal argument of correctness. Nuprl provides users with the facility for writing formal arguments and proof-generating programs in a well-known metalanguage, "ML". Users can employ Nuprl to create libraries of mathematical facts, definitions, theorems, and ML programs useful in generating proofs of theorems. For example, users supply the details of formal arguments and Nuprl checks the details of the argument from a verification perspective.
One of the main advantages and distinguishing features of Nuprl in this verification context stems from its highly expressive formal logic. In particular, many of Nuprl's theorem-proving benefits are an artifact of the technique's approach to so-called type theory. As will be appreciated, the "type" of an expression typically specifies some basic properties of the expression, e.g., the expression represents an integer value. The Nuprl programming language is widely recognized has having an extensive feature set for representing expression types very concisely and for representing a wide range of mathematical properties as types. The expressive power of Nuprl's type theory comes at a certain operational cost, that is, some of the traditional properties of type theories are not present. Indeed, Nuprl's approach to type theory is such that terms are viewed as "untyped", in the sense that one cannot determine from the syntax of an expression what, if any, type it is a member of. Thus, Nuprl's expressive power is advantageous in the verification of large-scale applications, such as certain protocol verification approaches, where the underlying formal mathematics is highly complicated.
However, while Nuprl's expressive power is a significant advantage, Nuprl's type theory approach, i.e., untyped terms, can lead to less than optimal results in certain applications, in particular, where processing speed is more critical than expressive power. That is, in certain system verification applications it is sometimes important to have terms, i.e., expressions, have associated types therewith. For example, so-called "term rewriting" frequently occurs in verification systems where the system will manipulate expressions during the verification process and replace equivalent expressions. Such term rewriting relies significantly on the use and access to type information. This is due to the fact that term rewriting involves successive applications of rewrite rules, and such rules are only correct when instantiated with terms of particular types. For example, the rewrite rule "x+0=x" is only valid in Nuprl when x is replaced by an expression of the type "integer". Thus, whenever this rule is applied, it must be verified that the expression for x has type "integer". In Nuprl, in order to ensure soundness of the inference mechanism, all properties must be proved such that each application of a rewrite rule will involve proofs that any expression substituted for variables of the rule has the type specified by that variable. As Nuprl's type theory mechanism is one where terms are basically untyped, its verification effectiveness in applications requiring speed over expressive power, e.g., applications employing term rewriting, is diminished.
Therefore, a need exists for a technique that allows for improved term rewriting while maintaining the expressive type properties of Nuprl in verification applications.